COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	fetch zf.ax[w78,jmc]
C00003 ENDMK
C⊗;
fetch zf.ax[w78,jmc];
fetch equiv.ax;
∧i REPL[A←λx s.(∀y.(yεs ≡ yεa ∧ R(x,y)))];
∧i REPL[A←λx t.(∀y.(yεt ≡ yεa ∧ R(x,y)))];
1  ∀x.∃y.∀z.(∀y.(yεz≡(yεa∧R(x,y)))≡y=z)⊃∀u.∃v.∀r.(rεv≡∃s.(sεu∧∀y.(yεr≡(yεa∧R(r,y)))))    ∧I REPL
2  ∀x.∃y.∀z.(∀y.(yεz≡(yεa∧R(x,y)))≡y=z)⊃∀u.∃v.∀r.(rεv≡∃s.(sεu∧∀y.(yεr≡(yεa∧R(s,y)))))    ∧I REPL